\begin{tabbing}
chain{-}config(${\it es}$;${\it Sys}$;${\it chain}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+\+
\\[0ex]no\_repeats(Id;${\it chain}$($e$)) \& (0 $<$ $\parallel$${\it chain}$($e$)$\parallel$) \& (es{-}loc(${\it es}$; $e$) $\in$ ${\it chain}$($e$) $\in$ Id))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$), ${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]sublist(Id; (${\it chain}$($e$)); (${\it chain}$(${\it e'}$))) $\vee$ sublist(Id; (${\it chain}$(${\it e'}$)); (${\it chain}$($e$))))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$), ${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]es{-}locl(${\it es}$; $e$; ${\it e'}$) $\Rightarrow$ sublist(Id; (${\it chain}$(${\it e'}$)); (${\it chain}$($e$))))
\-\-
\end{tabbing}